)

See #3742 for full context; this PR adds a backwards-compatible check
for `symbol'Kywd` as well as `klabel` for the pseudo-builtin sorts
`Endianness` and `Signedness`. When this is merged, I'll be able to
finish working on runtimeverification/k#4045.
Then, when that PR lands, the frontend will no longer emit `klabel(_)`
to KORE, and we can safely remove the backwards-compatible part of this
PR.

The integration test suite's checked-in KORE files are all updated to
use the new attribute rather than the old one, but the tests that use K
to compile fresh KORE will still be using `klabel(_)` until the
dependency update job induced by the changes above goes through.

I have verified manually that building K with this HB commit allows the
failing integration test in #3742 to pass.

Thanks @jberthold for the suggestions!

~~The implementation here would ideally be made backwards-compatible; my
version induces a dependency loop (hence failing tests, it would need an
update to the K dependency to go through first for the integration test
suite to pass).~~

When working on #4045, I identified a case in the C Semantics where an
overload set was flagged as being singletons (that is, that the
productions in the set were not actually overloads of one another).
Despite this warning, removing the `overload(_)` attributes broke
compilation by producing a parsing ambiguity.

It turns out that the issue was a difference between the main module and
the _disambiguation module_ produced during the inner parsing process.
The disambiguation module adds an additional production
```
Es ::= E
```
for user list sorts `Es` that subsorts the list element sort into the
list sort. This means that two productions
```
S ::= f(Es)
T ::= f(E)
```
can be overloads of one another.

However, this check was only using the overloads induced by the main
module and not those used by the disambiguation module. The fix is
simply to compute the disambiguation module[^1] and use its overloads
for the checks. Doing so requires some changes to the plumbing; the
subsorting production is previously only added when `RULE-LISTS` is
imported, but we need to short-circuit that code path in this context.

This PR includes a regression test minimised from the original example.

[^1]: I tried a cheaper fix that just checks parameters of
overload-attributed productions to see if they appear in a user list,
but this isn't sufficiently general in the case where the overload
parameter is actually a sub-/supersort of the user list element, as
happens in the C semantics.

When working on #4045, I noticed that a pair of productions like:
```k
syntax KItem ::= disambiguate(KItem, KItem) [overload(disambiguate)]
               | disambiguate(List,  Set)   [overload(disambiguate)]
```
were both being incorrectly flagged as singleton overloads, despite
meeting the criteria for being an overload set.

Some investigation reveals that this is due to the overload lattice
checks being applied _before_ the compiler inserts subsorting
productions into `KItem` for every sort; we therefore don't know that
`List <: KItem` when constructing the overload lattice.

The solution is to move the overload checks later in the compilation
process, after the compilation pipeline has been run. This PR makes that
change, along with some associated documentation and renaming for
clarity. It also includes a regression test with the example above; I
have verified that the test breaks before this PR.

Related:
* #4045
* runtimeverification/kontrol#679

Changes:
* Remove `Atts.KLABEL`
* Make `Atts.SYMBOL` unary